// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_MATH_VECTOR_MEMORY
#define _sHT_MATH_VECTOR_MEMORY

#include <stdint.h>

/*@ // Description: lift a C array of T to a logic vector of T
    // Consistency status: manual, checked, unverified
    axiomatic VectorMemory8 {
      // TODO: extend Frama-C to allow polymorphism
      // restricted to certain classes of types, e.g.
      // C types or just integral C types.
      logic \list<ℤ> vector_load_u8{L1}(uint8_t *c, ℤ n)
        reads c[0 .. n - 1];

      axiom vector_load_length_u8{L1}: ∀ uint8_t *c, ℤ n;
        0 <= n ==> \length(vector_load_u8(c, n)) == n;
      axiom vector_load_at_u8{L1}: ∀ uint8_t *c, ℤ n, i;
        0 <= i < n ==> \nth(vector_load_u8(c, n), i) == \at(c[i], L1);

      lemma vector_load_peelr_u8{L1}: ∀ uint8_t *c, ℤ n;
        0 <= n ==> vector_load_u8(c, n + 1) == (vector_load_u8(c, n) ^ [| c[n] |]);
    } */

#endif
